Regular expression matching using backtracking can have exponential runtime,leading to an algorithmic complexity attack known as REDoS in the systemssecurity literature. In this paper, we build on a recently published staticanalysis that detects whether a given regular expression can have exponentialruntime for some inputs. We systematically construct a more accurate analysisby forming powers and products of transition relations and thereby reducing theREDoS problem to reachability. The correctness of the analysis is proved usinga substructural calculus of search trees, where the branching of the treecausing exponential blowup is characterized as a form of non-linearity.
展开▼
